// Assignment 1
// Indication of time spent: 3 man hours
// 
// John likes all girls. 
// Some girl likes everybody but John. 
// Mary likes only John.
// No boy except John likes every girl.

abstract sig Person { }
abstract sig Boy extends Person { likes: set Girl }
abstract sig Girl extends Person { likes: set Boy }

one sig John extends Boy { }
sig OtherBoy extends Boy { }
one sig Mary extends Girl { }
sig OtherGirl extends Girl { }

fact everyBoyLikesSomeone {
  no b: Boy | b.likes = none
}

fact everyGirlLikesSomeone {
  no g: Girl | g.likes = none
}

fact johnLikesAllGirls {
  all g: Girl | g in John.likes
}

fact maryLikesOnlyJohn {
  no ob: OtherBoy | ob in Mary.likes
}

fact someGirlLikesEverybodyButJohn {
  some g:Girl | OtherBoy in g.likes and not John in g.likes
}

fact noBoyButJohnLikesEveryGirl {
  all ob:OtherBoy | not Girl = ob.likes
}

pred isJohnOnlyBoy {
  // According to this predicate there is no instance where John is the
  // only boy. This is correct. The rule "some girls like everybody but
  // John" cannot be realized if there are no boys but John, assuming
  // everyone likes at least one person (which is implied by the riddle).
  not (Boy - John) = none
}

run isJohnOnlyBoy for 6 Person
